i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), A:ecl(ds; da), snd:msg-spec(ds; da),
upd:update-spec(ds; da).
msg-spec-loc(snd; i)
 update-spec-decl(upd; ds)
 ((fpf-dom(id-deq; mkid{ecl:ut2}; ds)))
 R-Feasible{i:l}
 R-Feasible(ecl-machine{ecl:ut2}(i; ds; da; A; snd; upd))
 (B:es_realizer{i:l}. 
 R-Feasible{i:l}
 R-Feasible(B)
  l_all(append(ecl-kinds(A); fpf-domain(da));
  l_all(Knd;
  l_all(k.((isrcv(k))
  l_all( (((source(lnk(k)) = i  Id)
  l_all(  subtype_rel(ma-valtype(da; k);
  l_all(  subtype_rel(fpf-cap(R-da(B; destination(lnk(k))); Kind-deq; k; top)))
  l_all(  ((destination(lnk(k)) = i  Id)
  l_all(   subtype_rel(fpf-cap(R-da(B; source(lnk(k))); Kind-deq; k; void);
  l_all(   subtype_rel(fpf-cap(da; Kind-deq; k; void))))))
  R-icompat(ecl-machine{ecl:ut2}(i; ds; da; A; snd; upd); B)) 

latex

Definitions

ff, tt, if b then t else f fi , top, fpf-cap(f; eq; x; z), ma-valtype(da; k), x. t(x), prop{i:l}, t  T, fpf-all(A; eq; f; x,v.P(x;v)), x:A. B(x), P  Q, l_all(L; T; x.P(x)), mkid{$x:ut2}, P  Q, Id, x:A. B(x), Unit, , fpf-compatible(A; a.B(a); eq; f; g), P  Q, P  Q, x(s),

Lemmas

assert of bnot, eqff to assert, bnot wf, iff transitivity, eqtt to assert, subtype rel transitivity, ecl-machine-R-da-dom, member append, ecl wf, msg-spec wf, update-spec wf, msg-spec-loc wf, update-spec-decl wf, id-deq wf, not wf, es realizer wf, R-Feasible wf, ma-valtype wf, Id wf, fpf-domain wf, ecl-kinds wf, append wf, l member wf, Knd wf, fpf-cap wf, fpf-ap wf, R-has-loc wf, bool wf, top wf, fpf wf, fpf-trivial-subtype-top, R-da wf, Kind-deq wf, fpf-dom wf, isrcv wf, assert wf, ldst wf, lnk wf, lsrc wf, ecl-machine-R-da, eq id wf, ecl-machine-loc, ecl-machine wf, R-icompat-one-loc